High dependability and reliability is a goal of all computer and software systems. Complex systems in general cannot attain high dependability without addressing crucial remaining open issues of software dependability. The need for ultra-high dependable systems increases continually, along with a corresponding increasing need to ensure correctness in system development.
The development of a system can begin with the development of a requirements specification, such as a formal specification or an informal specification. A formal specification might be encoded in a high-level language, whereas requirements in the form of an informal specification can be expressed in restricted natural language, “if-then” rules, graphical notations, English language, programming language representations, flowcharts, scenarios or even using semi-formal notations such as unified modeling language (UML) use cases.
Requirement specifications in terms of individual traces are by nature very partial and represent only the most prominent situations. This partiality is one of the major problems in requirement engineering. Partiality often causes errors in the system design that are difficult to fix. Thus, techniques to improve the partiality of requirements specifications are of major practical importance.
After completion of a requirements specification that represents domain knowledge, the system is developed. A formal specification may not necessarily be used by the developer in the development of a system. In the development of some systems, computer readable code is generated. The generated code can be encoded in a computer language, such as a high-level computer language. Examples of such languages include Java, C, C Language Integrated Production System (CLIPS), and Prolog.
In another aspect of conventional systems, sensor networks perform any number of different tasks, among them planetary and solar system exploration. An example of a sensor network for solar system exploration is the Autonomous Nano Technology Swarm mission (ANTS), which will send 1,000 pico-class (approximately 1 kg) spacecraft to explore the asteroid belt. The ANTS spacecraft acts as a sensor network making observations of asteroids and analyzing composition of the asteroids. Sensor networks are also applicable for planetary (e.g., Martian) exploration, to yield scientific information on weather and geology. For Earth exploration missions, sensor networks are applicable to early warnings about natural disasters and climate change.
NASA sensor networks can be highly distributed autonomous “systems of systems” that must operate with a high degree of reliability. The solar system and planetary exploration networks necessarily experience long communications delays with Earth. The exploration networks are partly and occasionally out of touch with the Earth and mission control for long periods of time, and must operate under extremes of dynamic environmental conditions. Due to the complexity of these systems as well as the distributed and parallel nature of the exploration networks, the exploration networks have an extremely large state space and are impossible to test completely using traditional testing techniques. The more “code” or instructions that can be generated automatically from a verifiably correct model, the less likely that human developers will introduce errors. In addition, the higher the level of abstraction that developers can work from, as is afforded through the use of scenarios to describe system behavior, the less likely that a mismatch will occur between requirements and implementation and the more likely that the system can be validated. Working from a higher level of abstraction also provides that errors in the system are more easily caught, since developers can more easily see the “big picture” of the system. Conventional systems also do not capture expert knowledge from natural language description through to low-level implementations, such as implementations in CLIPS, while maintaining correctness. In addition, conventional systems usually require other ways to validate procedures, for example from the Hubble Robotic Servicing Mission (HRSM), i.e. the procedures for replacement of cameras on the Hubble Space Telescope (HST). Furthermore, a test-based model generation by classical automata learning is very expensive, and requires an impractically large number of queries to the system, each of which must be implemented as a system-level test case. In particular trace-combination methods of testing have proven to be expensive.
For the reasons stated above, and for other reasons stated below which will become apparent to those skilled in the art upon reading and understanding the present specification, there is a need in the art to reduce partiality of system requirement specifications, reduce system development time, reduce the amount of testing required of a new system, and improve confidence that the system reflects the requirements. There is also a need to develop systems starting at higher levels of abstraction.